D:dsys{i:l}, P:({es:ES{i}| d-es{i:l}(D; es)} {i'}).
d-realizes2{i:l}(D; es.P(es))  d-realizes{i:l}(D; es.P(es)) 

latex

Definitions	x:A. B(x), , P  Q, x(s), D realizes es. P(es), t  T, x. t(x), D realizes2 es.P(es)
Lemmas	possible-world wf, fair-fifo wf, world wf, d-sub wf, dsys wf, d-realizes2 wf, event system wf, d-es wf, possible-world-monotonic